Nuprl Lemma : eq_ds_wf
11,40
postcript
pdf
A
:Type,
d
:DS(
A
),
a
:
A
,
x
,
y
:dstype(
A
;
d
;
a
).
x
=
y
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
x
=
y
Lemmas
dseq
wf
,
dstype
wf
,
discrete
struct
wf
origin
A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). x = y 
A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). x = y x:A. B(x) T